T, T':Type{i}, L:(T List), f:({t:T| (t  L)} T'), P:(T'T'{i'}).
(x,ymap(f;L).  P(x,y))  (x,yL.  P(f(x),f(y))) 

latex

Definitions	Type, , t  T, x:AB(x), x:A. B(x), (x  l), {x:A| B(x)} , type List, f(a), x(s1,s2), x,y. t(x;y), (x,yL.  P(x;y)), map(f;as), P  Q, P  Q, S  T, suptype(S; T), x:A  B(x), P & Q, P  Q, ||as||, False, A, A  B, i  j < k, , {i..j}, a < b, Void, x:A.B(x), Top, l[i]
Lemmas	select wf, list-set-type, map-wf2, select-map, le wf, length-map, map wf, pairwise wf